Problem:
 f(nil()) -> nil()
 f(.(nil(),y)) -> .(nil(),f(y))
 f(.(.(x,y),z)) -> f(.(x,.(y,z)))
 g(nil()) -> nil()
 g(.(x,nil())) -> .(g(x),nil())
 g(.(x,.(y,z))) -> g(.(.(x,y),z))

Proof:
 Bounds Processor:
  bound: 1
  enrichment: match
  automaton:
   final states: {4,3}
   transitions:
    g1(12) -> 14*
    g1(7) -> 14*
    g1(2) -> 14*
    g1(16) -> 14,4
    g1(1) -> 14*
    .1(2,12) -> 8*
    .1(3,5) -> 5,3
    .1(16,2) -> 16*
    .1(1,2) -> 7*
    .1(1,8) -> 8*
    .1(1,12) -> 8*
    .1(12,1) -> 16*
    .1(7,1) -> 16*
    .1(2,1) -> 7*
    .1(2,7) -> 8*
    .1(14,3) -> 14,4
    .1(16,1) -> 16*
    .1(1,1) -> 12*
    .1(1,7) -> 8*
    .1(12,2) -> 16*
    .1(7,2) -> 16*
    .1(2,2) -> 7*
    .1(2,8) -> 8*
    nil1() -> 14,5,4,3
    f1(12) -> 5*
    f1(7) -> 5*
    f1(2) -> 5*
    f1(1) -> 5*
    f1(8) -> 5,3
    f0(2) -> 3*
    f0(1) -> 3*
    nil0() -> 1*
    .0(1,2) -> 2*
    .0(2,1) -> 2*
    .0(1,1) -> 2*
    .0(2,2) -> 2*
    g0(2) -> 4*
    g0(1) -> 4*
  problem:
   
  Qed